L:(Top List), n:{0..(||L||+1)}. L ~ (firstn(n;L) @ nth_tl(n;L)) 

latex

Definitions	Top, t  T, {i..j}, x:A. B(x), i <z j, i z j, P & Q, i  j < k, P  Q, False, A, A  B, {T}, SQType(T), , nth_tl(n;as), ||as||, True, b, b, , T, P  Q, P  Q, Unit, i  j , tl(l)
Lemmas	bnot of le int, length cons, non neg length, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, lt int wf, le wf, bool wf, bnot wf, assert wf, le int wf, length wf1, int seg wf, top wf